% 
% 
% \section{Mobile phone battery example}\label{ex:battery}
%   %
%       Take the battery of a mobile phone.  We identify its
%       electric capacity as an entity having a few charge levels. For the
%       sake of the example, say $5$ levels from $0$ the minimal level of
%       charge to $4$ meaning full charge. The evolution of the charge
%       level along time is subject to the following constraints:
%       \begin{enumerate}
% 
%       \item \label{it:decay} The level of mobile phone charge diminishes
%             continuously, even when it is not used for making a phone
%             call; it diminishes slowly when it is fully charged and
%             faster when it is partly discharged;
% 
%       \item \label{it:plug} The mobile phone may be plugged to start
%             charging, which takes some time to reach full charge;
% 
%       \item \label{it:call} If charged enough, the mobile phone may be
%             used to make phone calls but its charge diminishes;
% 
%       \item \label{it:GPS} Similarly, GPS navigation needs more charge
%             and consumes battery faster.
%       \end{enumerate}
%       Item~(\ref{it:decay}) corresponds to the decay process, while the
%       other three items represent activity rules. Item (\ref{it:plug})
%       is modeled with an auxiliary entity representing the plug (which
%       may be on or off). The action of plugging the mobile phone is a
%       \potential activity. If plugged the battery starts charging which
%       is represented by a \obligatory activity augmenting its charge
%       level. Items~(\ref{it:call}) and~(\ref{it:GPS}) are implemented
%       similarly, using two more entities one for the call and the other
%       for the GPS navigation.   
% 
%  \paragraph{\bf Entities.}     A mobile phone is characterized by four observables with corresponding number of levels and associated decay:
%       $$ \begin{array}{rcll}
%             \text{Battery}  
%             & ~~B~~ 
%             & \setlev_{B} = 5
%             & \life_{B}(i)=2 \text{ for }  0<i \leq 3,  \quad
%             \life_{B}(4)=3
%             \\
%             \text{Plug} 
%             & P 
%             & \setlev_{P} = 2 
%             &  
%             \\
%             \text{Call} 
%             & C 
%             & \setlev_{C} = 2 
%             &  
%             \\
%             \text{GPS} 
%             & G 
%             & \setlev_{G} = 2 \ 
%             &  
%       \end{array}
%       $$
%       %%
%       where unspecified decays are all set to $\omega$.  Decay
%       durations are used to model Item (\ref{it:decay}) above. Notice that in the modeling of charge $B$,
%       delays are not uniform to denote different speeds in the
%       consumption of the charge (\ie for the full charge level 4 decay
%       takes 3 units of time while for the others it is 2).  All other
%       entities have only two levels, roughly speaking
%       \emph{on}/\emph{off}, encoded as 0 for \emph{off} and 1 for
%       \emph{on}. The environment has no role in the evolution of the
%       levels of these observables that are therefore set to unbounded
%       duration $\omega$.  
% 
% \paragraph{\bf Activities.}      The constraints specified by Items (2-4) above give rise to the following sets of
%       activities.
% 
%       Item (\ref{it:plug}) may be described by two \potential
%       instantaneous activities, $\alpha_1$ and $\alpha_2$, which model
%       plugging and unplugging respectively, and a \obligatory activity
%       $\beta_1$ with duration 1 that models the charging process.
%       $$
%       \begin{array}{ll ll}
%         \alpha_1: & \activ{(P,0)}{(P,1)}{0}{(P,+1)} 
%         \qquad & \beta_1: & \activ{(P,1)}{\emptyset}{1}{(B,+1)}  \\
%          \alpha_2: & \activ{(P,1)}{\emptyset}{0}{(P,-1)}   
%       \end{array}
%       $$
% 
%       Similarly, Item (\ref{it:call}) may be depicted by two
%       \potential instantaneous activities, $\alpha_3$ and $\alpha_4$,
%       modeling the start and the end of a phone call respectively, and
%       a \obligatory activity $\beta_2$ with duration 3 defining the
%       discharging process due to such a call.\looseness=-1
%       %% 
%       $$
%       \begin{array}{ll ll}
%             \alpha_3: & \activ{(C,0)}{(C,1)}{0}{(C,+1)} 
%             \qquad & \beta_2: & \activ{(C,1)}{\emptyset}{3}{(B,-1)} \\
%             \alpha_4: & \activ{(C,1)}{\emptyset}{0}{(C,-1)} 
%       \end{array}
%       $$
% 
%       Finally Item (\ref{it:GPS}) may again be described by two
%       \potential instantaneous activities, $\alpha_5$ and $\alpha_6$,
%       that model activation and deactivation of GPS navigation
%       respectively, and a \obligatory activity $\beta_3$ with
%       duration 3 that models the discharging process due to the GPS
%       usage. Notice that in this case, even if duration is the same,
%       the battery is consumed faster than a simple phone call
%       (indicated by $(B, -2)$ instead of $(B, -1)$).
%       $$
%       \begin{array}{ll ll}
%             \alpha_5: & \activ{(G,0)}{(G,1)}{0}{(G,+1)}
%             \qquad &  \beta_3: & \activ{(G,1)}{\emptyset}{3}{(B,-2)} \\
%             \alpha_6: & \activ{(G,1)}{\emptyset}{0}{(G,-1)} 
%       \end{array}
%       $$
%       \paragraph{\bf Initial state and execution
%       scenario.}
% 			
% We illustrate the functioning of an \andy network on the
% following scenario starting from the initial levels: 
% $(B, 4)$, $(P, 0)$, $(C, 0)$, $(G,0)$, see Figure~\ref{fig:diagram}:
% 
% 
% 
% \begin{figure}[t]
% \centering
% \begin{tikzpicture}[>=latex',xscale=.8, yscale=.5]
% 
% \draw[draw=none,fill=blue!10] (-1,1) rectangle (11,2) ; 
% \draw[draw=none,fill=blue!10] (-1,3) rectangle (11,4) ; 
% \draw[draw=none,fill=blue!10] (-1,5) rectangle (11,6) ; 
% \draw[draw=none,fill=blue!10] (-1,7) rectangle (11,8) ; 
% \draw[draw=none,fill=blue!10] (-1,9) rectangle (11,10) ; 
% 
% \node at (-1,1) (p0) {};
% \node[left] at (p0.west) {$0$};
% \node at (-1,2) (p1) {};
% \node[left] at (p1.west) {$1$};
% \node at (-1,3) (c0) {};
% \node[left] at (c0.west) {$0$};
% \node at (-1,4) (c1) {};
% \node[left] at (c1.west) {$1$};
% \node at (-1,5) (g0) {};
% \node[left] at (g0.west) {$0$};
% \node at (-1,6) (g1) {};
% \node[left] at (g1.west) {$1$};
% \node at (-1,7) (b0) {};
% \node[left] at (b0.west) {$0$};
% \node at (-1,8) (b1) {};
% \node[left] at (b1.west) {$1$};
% \node at (-1,9) (b2) {};
% \node[left] at (b2.west) {$2$};
% \node at (-1,10) (b3) {};
% \node[left] at (b3.west) {$3$};
% 
% \node[label=left:{$B=\left[ \phantom{\begin{array}{l} a\\ a\\ a\\ a \end{array}} \right.$}] at (-1,8.5) (b) {};
% \node[label=left:{$G=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,5.5) (g) {};
% \node[label=left:{$C=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,3.5) (c) {};
% \node[label=left:{$P=\left[ \phantom{\begin{array}{l} a\\ a \end{array}} \right.$}] at (-1,1.5) (p) {};
% 
% %\draw[->] (p0) -- (p1) ;
% %\draw[->] (c0) -- (c1) ;
% %\draw[->] (g0) -- (g1) ;
% %\draw[->] (b0) -- (b3) ;
% 
% %points horizontaux
% \node at (-2,0) (t0) {};
% \node[rectangle,draw,fill=blue,scale=.3,label=below:0] at (0,0) (t1) {};
% \node[rectangle,draw,fill=blue,scale=.3,label=below:1] at (2,0) (t2) {};
% \node[rectangle,draw,fill=blue,scale=.3,label=below:2] at (4,0) (t3) {};
% \node[rectangle,draw,fill=blue,scale=.3,label=below:3] at (6,0) (t4) {};
% \node[rectangle,draw,fill=blue,scale=.3,label=below:4] at (8,0) (t5) {};
% \node[rectangle,draw,fill=blue,scale=.3,label=below:5] at (10,0) (t6) {};
% \node[label=below:$time$] at (11,0) (t7) {};
% 
% % points verticaux
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,1) (k1) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,2) (k2) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,3) (k3) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,4) (k4) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,5) (k5) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,6) (k6) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,7) (k7) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,8) (k8) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,9) (k9) {};
% \node[rectangle,draw,fill=blue,scale=.3] at (-1,10) (k10) {};
% 
% \draw[->] (t0) -- (t7) ; %axe du temps
% \draw[->] (-1,0) -- (-1,11.5) ; %axe vertical
% 
% \path[draw,thick] (0,1) --(6,1) --node[midway,above,sloped]{$\alpha_1$} (6,2) -- (9,2) ;
% \node[right] at (9,2) {$\cdots$};
% \path[draw,thick] (0,3)  --node[midway,above,sloped]{$\alpha_3$} (0,4) -- (9,4) ;
% \node[right] at (9,4) {$\cdots$};
% \path[draw,thick] (0,5) --node[midway,above, sloped]{$\alpha_5$}  (0,6) -- (9,6) ;
% \node[right] at (9,6) {$\cdots$};
% \path[draw,thick] (0,10) -- (6,10) -- (6,7) -- (8,7) -- (8,9) -- (9,9) ;
% \node[right] at (9,9) {$\cdots$};
% \node[above] at (6,10) {$\beta_2,\beta_3,decay$};
% \node[above] at (8,9) {$\beta_1$};
% 
% \end{tikzpicture}
% \caption{Entities levels evolving with time corresponding to the given scenario.}
% \label{fig:diagram}
% \end{figure}
% 
%       \begin{enumerate}
% 
%       \item Activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)
% 
%       \item Start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)
% 
%       \item Three time units pass by -- no decay or \obligatory activities are involved
% 
%       \item One time unit passes by -- battery decays and enabled \obligatory
%             activities\\
%             %
%             $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}$ and
%             $\beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$
%             %
%             are performed
% 
%       \item Plug the phone ($\alpha_1: \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)
% 
%       \item One time unit passes by -- no decay but enabled
%         \obligatory activity
%         $\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed 
%       \end{enumerate}
%       
% 
% 
% \paragraph{\bf  Execution scenario.}
% We illustrate the evolution of tuples of counters $\birth{}$ starting from 
% the initial state, we have the following sequence of markings:
% $$
% \begin{array}{ccccc}
%  & p_B &p_P&p_C&p_G\\
% \mathit{init} & \quad \tuple{4, 0, [0,0,0,0,0]} \quad 
%  & \quad \tuple{0, 0, [0,0]} \quad 
%  &\quad  \tuple{0, 0, [0,0]}\quad 
%  &\quad  \tuple{0, 0, [0,0]}\quad \\
% %we activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)
% 1 & \quad \tuple{4, 0, [0,0,0,0,0]}\quad
%  &\quad \tuple{0, 0, [0,0]}\quad
% &\quad \tuple{0, 0, [0,0]}\quad
%  &\quad \tuple{1, 0, [0,0]}\quad \\
% %start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)
% 2 & \quad \tuple{4, 0, [0,0,0,0,0]} \quad
% & \quad \tuple{0, 0, [0,0]} \quad
%  &\quad \tuple{1, 0, [0,0]}\quad
%  &\quad \tuple{1, 0, [0,0]}\quad \\
% %3 time units pass by (no decay or obligatory activity involved)
% 3 & \quad
%  \tuple{4, 3, [3,3,3,3,3]} \quad
% & \quad \tuple{0, 0, [3,3]} \quad
% & \quad \tuple{1, 0, [3,3]} \quad
% & \quad \tuple{1, 0, [3,3]}\quad \\
% % 1 time unit pass by, battery decays, and enabled obligatory activities\\ $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}, \beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$ are performed
% 4 & \quad
%  \tuple{0, 0, [0,0,0,0,0]} \quad
% & \quad \tuple{0, 0, [3,3]}\quad
% & \quad \tuple{1, 0, [3,3]}\quad
% & \quad \tuple{1, 3, [3,3]}\quad \\
% %we plug the phone ($\alpha_1:  \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)
% 5 & \quad
%  \tuple{0, 0, [0,0,0,0,0]} \quad
% & \quad \tuple{1, 0, [3,0]} \quad
% & \quad \tuple{1, 0, [3,3]} \quad
% & \quad \tuple{1, 0, [3,3]} \quad \\
% % 1 time unit passes by with no decays and enabled obligatory activity\\
% %\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed
% 6 & \quad
%  \tuple{1, 0, [1,0,1,1,1]} \quad
%  &\quad \tuple{1, 0, [3,1]} \quad
%  &\quad \tuple{1, 0, [3,3]} \quad
%  &\quad \tuple{1, 0, [3,3]} 
% \end{array}
% $$
% 
% Figure \ref{fig:snakesbattery} shows the SNAKES Petri net rendering of the mobile phone example.
% 
% \begin{figure}[t]
% 
% 
% {\centering
% \scalebox{0.33}{
% \begin{tikzpicture}[>=latex',line join=bevel,scale=0.7]
% %%
% \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_13) at (1218.6bp,361bp) [draw,fill=fillcolor,rectangle] {tr1};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_14) at (1206.6bp,151bp) [draw,fill=fillcolor,rectangle] {tr0};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_18) at (943.65bp,571bp) [draw,fill=fillcolor,rectangle] {tc: True};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_19) at (714.65bp,361bp) [draw,fill=fillcolor,rectangle] {tr4};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_9) at (1393.6bp,676bp) [draw,fill=fillcolor,ellipse] {ptr0: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_8) at (331.65bp,466bp) [draw,fill=fillcolor,ellipse] {ptr3: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_7) at (520.65bp,46bp) [draw,fill=fillcolor,ellipse] {ptr2: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_6) at (851.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob2: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_5) at (1006.6bp,466bp) [draw,fill=fillcolor,ellipse] {ptr4: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_4) at (103.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob0: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_3) at (219.65bp,466bp) [draw,fill=fillcolor,ellipse] {pob1: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_2) at (699.65bp,256bp) [draw,fill=fillcolor,ellipse] {G: \{(0, 0, (0, 0))\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_1) at (663.65bp,466bp) [draw,fill=fillcolor,ellipse] {B: \{(4, 0, (0, 0, 0, 0, 0))\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_0) at (183.65bp,256bp) [draw,fill=fillcolor,ellipse] {C: \{(0, 0, (0, 0))\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_17) at (745.65bp,151bp) [draw,fill=fillcolor,rectangle] {tr5};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_11) at (887.65bp,46bp) [draw,fill=fillcolor,ellipse] {ptr5: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_16) at (282.65bp,151bp) [draw,fill=fillcolor,rectangle] {tr2};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_10) at (1226.6bp,466bp) [draw,fill=fillcolor,ellipse] {ptr1: \{0\}};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_15) at (209.65bp,361bp) [draw,fill=fillcolor,rectangle] {tr3};
%   \definecolor{fillcolor}{rgb}{1.0,1.0,1.0};
%   \node (node_12) at (1158.6bp,256bp) [draw,fill=fillcolor,ellipse] {P: \{(0, 0, (0, 0))\}};
%   \draw [->,solid] (node_4) ..controls (53.011bp,500.46bp) and (38.13bp,517.88bp)  .. (51.647bp,532bp) .. controls (81.223bp,562.9bp) and (723bp,569.51bp)  .. (node_18);
%   \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
%   \pgfsetstrokecolor{strokecol}
%   \draw (75.647bp,523bp) node { $wob_0$};
%   \draw [->,solid] (node_18) ..controls (1038.5bp,561.15bp) and (1159.3bp,546.66bp)  .. (1171.6bp,532bp) .. controls (1176.8bp,525.88bp) and (1175.9bp,520.78bp)  .. (1171.6bp,514bp) .. controls (1161.9bp,498.5bp) and (1148.7bp,507.72bp)  .. (1134.6bp,496bp) .. controls (1109.3bp,474.81bp) and (1118.7bp,453.59bp)  .. (1090.6bp,436bp) .. controls (1053.5bp,412.68bp) and (1021.7bp,451.71bp)  .. (993.65bp,418bp) .. controls (993.65bp,418bp) and (993.65bp,340bp)  .. (993.65bp,340bp) .. controls (970.26bp,310.93bp) and (935.71bp,350.52bp)  .. (911.65bp,322bp) .. controls (897.88bp,305.68bp) and (905.03bp,151.22bp)  .. (902.65bp,130bp) .. controls (901bp,115.31bp) and (898.36bp,99.311bp)  .. (node_11);
%   \draw (969.65bp,313bp) node { min(D,wtr5+1)};
%   \draw [->,solid] (node_5) ..controls (964.3bp,442.46bp) and (955.34bp,438.64bp)  .. (946.65bp,436bp) .. controls (885.78bp,417.51bp) and (864.51bp,439.53bp)  .. (804.65bp,418bp) .. controls (785.12bp,410.97bp) and (765.42bp,399.16bp)  .. (node_19);
%   \draw (815.65bp,409bp) node { w};
%   \draw [->,solid] (node_9) ..controls (1265.4bp,646.08bp) and (1074.2bp,601.47bp)  .. (node_18);
%   \draw (1204.1bp,619bp) node { wtr0};
%   \draw [->,solid] (node_19) ..controls (733.51bp,329.2bp) and (737.44bp,315.93bp)  .. (733.65bp,304bp) .. controls (732.5bp,300.38bp) and (730.96bp,296.8bp)  .. (node_2);
%   \draw (798.15bp,313bp) node { ($l_G$,$u_G$,$\lambda_G$)};
%   \draw [->,solid] (node_18) ..controls (976.99bp,539.38bp) and (983.9bp,526.2bp)  .. (977.65bp,514bp) .. controls (971.41bp,501.81bp) and (961.45bp,506.49bp)  .. (952.65bp,496bp) .. controls (933.6bp,473.32bp) and (948.29bp,452.43bp)  .. (923.65bp,436bp) .. controls (893.74bp,416.06bp) and (636.01bp,424.46bp)  .. (600.65bp,418bp) .. controls (574.51bp,413.22bp) and (569.43bp,406.41bp)  .. (543.65bp,400bp) .. controls (522.16bp,394.66bp) and (459.82bp,399.01bp)  .. (445.65bp,382bp) .. controls (433.7bp,367.66bp) and (433.43bp,354.12bp)  .. (445.65bp,340bp) .. controls (482.09bp,297.89bp) and (519.87bp,346.96bp)  .. (569.65bp,322bp) .. controls (579.76bp,316.93bp) and (578.28bp,310.34bp)  .. (587.65bp,304bp) .. controls (600.65bp,295.2bp) and (615.53bp,287.46bp)  .. (node_2);
%   \draw (663.15bp,409bp) node { ($l_G$,$u_G$,$\lambda_G$)};
%   \draw [->,solid] (node_10) ..controls (1302.9bp,485.07bp) and (1346.3bp,499.1bp)  .. (1356.6bp,514bp) .. controls (1361.2bp,520.56bp) and (1362bp,526.08bp)  .. (1356.6bp,532bp) .. controls (1332.2bp,558.88bp) and (1089.5bp,567.62bp)  .. (node_18);
%   \draw (1382.1bp,523bp) node { wtr1};
%   \draw [->,solid] (node_8) ..controls (299.73bp,426.93bp) and (285.77bp,411.83bp)  .. (271.65bp,400bp) .. controls (266.54bp,395.72bp) and (260.92bp,391.56bp)  .. (node_15);
%   \draw (300.65bp,409bp) node { w};
%   \draw [->,solid] (node_18) ..controls (820.19bp,564.49bp) and (585.46bp,550.33bp)  .. (555.65bp,532bp) .. controls (502.72bp,499.46bp) and (554.78bp,442.7bp)  .. (509.65bp,400bp) .. controls (477.16bp,369.26bp) and (445.07bp,410.55bp)  .. (410.65bp,382bp) .. controls (382.83bp,358.93bp) and (372.19bp,336.67bp)  .. (387.65bp,304bp) .. controls (427.23bp,220.36bp) and (509.06bp,255.64bp)  .. (548.65bp,172bp) .. controls (562.05bp,143.68bp) and (552.46bp,108.7bp)  .. (node_7);
%   \draw (445.65bp,313bp) node { min(D,wtr2+1)};
%   \draw [->,solid] (node_14) ..controls (1381.8bp,177.1bp) and (1399.4bp,183.04bp)  .. (1408.6bp,190bp) .. controls (1435.1bp,209.78bp) and (1442.6bp,223bp)  .. (1442.6bp,256bp) .. controls (1442.6bp,571bp) and (1442.6bp,571bp)  .. (1442.6bp,571bp) .. controls (1442.6bp,597.2bp) and (1438.7bp,604.26bp)  .. (1427.6bp,628bp) .. controls (1425.6bp,632.45bp) and (1423.1bp,636.92bp)  .. (node_9);
%   \draw (1452.1bp,409bp) node { 0};
%   \draw [->,solid] (node_17) ..controls (795.99bp,113.78bp) and (825.8bp,91.734bp)  .. (node_11);
%   \draw (831.15bp,103bp) node { 0};
%   \draw [->,solid] (node_12) ..controls (1226bp,284.82bp) and (1235.5bp,293.33bp)  .. (1241.6bp,304bp) .. controls (1246.5bp,312.37bp) and (1245bp,321.95bp)  .. (node_13);
%   \draw (1309.1bp,313bp) node { ($l_P$, $u_P$, $\lambda_P$)};
%   \draw [->,solid] (node_17) ..controls (743.02bp,183.28bp) and (740.52bp,196.75bp)  .. (735.65bp,208bp) .. controls (733.99bp,211.82bp) and (731.98bp,215.61bp)  .. (node_2);
%   \draw (804.15bp,199bp) node { ($l_G$,$u_G$,$\lambda_G$)};
%   \draw [->,solid] (node_13) ..controls (1135.3bp,334.36bp) and (1123.9bp,328.18bp)  .. (1119.6bp,322bp) .. controls (1113.1bp,312.37bp) and (1115.6bp,301.62bp)  .. (node_12);
%   \draw (1178.6bp,313bp) node { ($l_P$,$u_P$,$\lambda_P$)};
%   \draw [->,solid] (node_16) ..controls (405.16bp,125.01bp) and (421.12bp,119.11bp)  .. (435.65bp,112bp) .. controls (454.06bp,103bp) and (472.29bp,89.591bp)  .. (node_7);
%   \draw (473.15bp,103bp) node { 0};
%   \draw [->,solid] (node_18) ..controls (1080.2bp,569.57bp) and (1378.7bp,563.5bp)  .. (1407.6bp,532bp) .. controls (1413.1bp,526.11bp) and (1411.5bp,521.02bp)  .. (1407.6bp,514bp) .. controls (1398.1bp,496.64bp) and (1267.1bp,435.36bp)  .. (1257.6bp,418bp) .. controls (1253.8bp,410.98bp) and (1252.4bp,406.08bp)  .. (1257.6bp,400bp) .. controls (1291.6bp,360.38bp) and (1338.7bp,420.76bp)  .. (1373.6bp,382bp) .. controls (1396.9bp,356.23bp) and (1398.4bp,331.04bp)  .. (1376.6bp,304bp) .. controls (1360.5bp,283.92bp) and (1302.4bp,271.75bp)  .. (node_12);
%   \draw (1316.6bp,409bp) node { ($l_P$,$u_P$,$\lambda_P$)};
%   \draw [->,solid] (node_11) ..controls (908.91bp,100.58bp) and (925.29bp,139.6bp)  .. (942.65bp,172bp) .. controls (975.6bp,233.51bp) and (1006.8bp,237.41bp)  .. (1027.6bp,304bp) .. controls (1042.8bp,352.38bp) and (999bp,379.22bp)  .. (1031.6bp,418bp) .. controls (1056.8bp,447.87bp) and (1087.2bp,411.53bp)  .. (1117.6bp,436bp) .. controls (1140.4bp,454.32bp) and (1124.6bp,474.67bp)  .. (1144.6bp,496bp) .. controls (1156.3bp,508.47bp) and (1169.8bp,499.35bp)  .. (1178.6bp,514bp) .. controls (1182.8bp,520.85bp) and (1183.8bp,525.9bp)  .. (1178.6bp,532bp) .. controls (1166.5bp,546.34bp) and (1053bp,559.99bp)  .. (node_18);
%   \draw (1053.1bp,313bp) node { wtr5};
%   \draw [->,solid] (node_18) ..controls (784.54bp,566.41bp) and (356.04bp,552.46bp)  .. (335.65bp,532bp) .. controls (328.73bp,525.06bp) and (325.98bp,515.41bp)  .. (node_8);
%   \draw (393.65bp,523bp) node { min(D,wtr3+1)};
%   \draw [->,solid] (node_0) ..controls (85.22bp,284.04bp) and (60.359bp,300.25bp)  .. (76.647bp,322bp) .. controls (80.619bp,327.3bp) and (89.039bp,332.13bp)  .. (node_15);
%   \draw (141.65bp,313bp) node { ($l_C$, $u_C$, $\lambda_C$)};
%   \draw [->,solid] (node_15) ..controls (210.44bp,328.99bp) and (209.61bp,315.62bp)  .. (206.65bp,304bp) .. controls (205.84bp,300.82bp) and (204.81bp,297.6bp)  .. (node_0);
%   \draw (270.15bp,313bp) node { ($l_C$,$u_C$,$\lambda_C$)};
%   \draw [->,solid] (node_7) ..controls (444.49bp,79.598bp) and (384.15bp,106.22bp)  .. (node_16);
%   \draw (420.65bp,103bp) node { w};
%   \draw [->,solid] (node_15) ..controls (227.95bp,393.76bp) and (237.57bp,407.73bp)  .. (248.65bp,418bp) .. controls (252.21bp,421.31bp) and (269.82bp,431.6bp)  .. (node_8);
%   \draw (258.15bp,409bp) node { 0};
%   \draw [->,solid] (node_12) ..controls (1115.8bp,300.47bp) and (1097.9bp,318.64bp)  .. (1093.6bp,322bp) .. controls (1081.4bp,331.62bp) and (1073.9bp,328.31bp)  .. (1063.6bp,340bp) .. controls (1050.6bp,354.9bp) and (1028.8bp,407.59bp)  .. (1037.6bp,418bp) .. controls (1068.8bp,454.82bp) and (1106.3bp,406.8bp)  .. (1144.6bp,436bp) .. controls (1168.1bp,453.82bp) and (1151.9bp,475.13bp)  .. (1172.6bp,496bp) .. controls (1175.1bp,498.48bp) and (1236.5bp,502.11bp)  .. (1210.6bp,532bp) .. controls (1196.3bp,548.59bp) and (1060bp,561.78bp)  .. (node_18);
%   \draw (1101.1bp,409bp) node { ($l_P$, $u_P$, $\lambda_P$)};
%   \draw [->,solid] (node_0) ..controls (282.79bp,277.88bp) and (311.35bp,288.61bp)  .. (334.65bp,304bp) .. controls (352.26bp,315.64bp) and (356.57bp,320.93bp)  .. (365.65bp,340bp) .. controls (380.78bp,371.8bp) and (360.63bp,388.35bp)  .. (379.65bp,418bp) .. controls (419.98bp,480.89bp) and (467.54bp,458.58bp)  .. (517.65bp,514bp) .. controls (523.78bp,520.79bp) and (519.98bp,527bp)  .. (527.65bp,532bp) .. controls (558.26bp,551.99bp) and (798.68bp,564.68bp)  .. (node_18);
%   \draw (444.65bp,409bp) node { ($l_C$, $u_C$, $\lambda_C$)};
%   \draw [->,solid] (node_2) ..controls (604.93bp,226.72bp) and (581.75bp,210.63bp)  .. (597.65bp,190bp) .. controls (601.83bp,184.57bp) and (610.33bp,179.75bp)  .. (node_17);
%   \draw (664.65bp,199bp) node { ($l_G$, $u_G$, $\lambda_G$)};
%   \draw [->,solid] (node_18) ..controls (760.09bp,567.16bp) and (169.47bp,553.4bp)  .. (136.65bp,532bp) .. controls (126.77bp,525.56bp) and (119.73bp,515.22bp)  .. (node_4);
%   \draw (160.65bp,523bp) node { $wob_0$};
%   \draw [->,solid] (node_11) ..controls (822.18bp,63.667bp) and (794.36bp,75.603bp)  .. (774.65bp,94bp) .. controls (766.85bp,101.27bp) and (760.83bp,111.11bp)  .. (node_17);
%   \draw (785.65bp,103bp) node { w};
%   \draw [->,solid] (node_14) ..controls (1223.1bp,183.15bp) and (1226.2bp,196.75bp)  .. (1220.6bp,208bp) .. controls (1217.9bp,213.69bp) and (1214bp,218.91bp)  .. (node_12);
%   \draw (1282.6bp,199bp) node { ($l_P$,$u_P$,$\lambda_P$)};
%   \draw [->,solid] (node_18) ..controls (749.02bp,569.86bp) and (73.172bp,563.87bp)  .. (42.647bp,532bp) .. controls (-27.86bp,458.37bp) and (-3.6588bp,376.85bp)  .. (67.647bp,304bp) .. controls (78.465bp,292.95bp) and (92.197bp,284.33bp)  .. (node_0);
%   \draw (66.147bp,409bp) node { ($l_C$,$u_C$,$\lambda_C$)};
%   \draw [->,solid] (node_16) ..controls (178.59bp,177.36bp) and (166.45bp,183.4bp)  .. (161.65bp,190bp) .. controls (155.67bp,198.2bp) and (155.99bp,208.13bp)  .. (node_0);
%   \draw (222.15bp,199bp) node { ($l_C$,$u_C$,$\lambda_C$)};
%   \draw [->,solid] (node_5) ..controls (996.74bp,507.27bp) and (991.71bp,520.89bp)  .. (984.65bp,532bp) .. controls (982.39bp,535.54bp) and (979.75bp,538.99bp)  .. (node_18);
%   \draw (1015.1bp,523bp) node { wtr4};
%   \draw [->,solid] (node_18) ..controls (966.39bp,604.78bp) and (979.81bp,619.84bp)  .. (995.65bp,628bp) .. controls (1054.2bp,658.14bp) and (1243.5bp,669.95bp)  .. (node_9);
%   \draw (1053.6bp,619bp) node { min(D,wtr0+1)};
%   \draw [->,solid] (node_19) ..controls (725.25bp,394.71bp) and (733.12bp,409.78bp)  .. (745.65bp,418bp) .. controls (783.13bp,442.61bp) and (903.5bp,423.76bp)  .. (946.65bp,436bp) .. controls (952.32bp,437.61bp) and (958.09bp,439.75bp)  .. (node_5);
%   \draw (755.15bp,409bp) node { 0};
%   \draw [->,solid] (node_1) ..controls (683.76bp,508.72bp) and (694.11bp,523.26bp)  .. (707.65bp,532bp) .. controls (738.58bp,551.97bp) and (839.92bp,562.99bp)  .. (node_18);
%   \draw (772.65bp,523bp) node { ($l_B$, $u_B$, $\lambda_B$)};
%   \draw [->,solid] (node_13) ..controls (1216.3bp,387.85bp) and (1215.9bp,394.16bp)  .. (1215.6bp,400bp) .. controls (1215.3bp,407.99bp) and (1214.7bp,410.05bp)  .. (1215.6bp,418bp) .. controls (1216bp,420.87bp) and (1216.4bp,423.81bp)  .. (node_10);
%   \draw (1225.1bp,409bp) node { 0};
%   \draw [->,solid] (node_2) ..controls (800.88bp,279.54bp) and (835.16bp,290.28bp)  .. (864.65bp,304bp) .. controls (877.72bp,310.08bp) and (878.31bp,316.51bp)  .. (891.65bp,322bp) .. controls (930.17bp,337.86bp) and (957.17bp,307.83bp)  .. (983.65bp,340bp) .. controls (995.51bp,354.41bp) and (995.94bp,367.95bp)  .. (983.65bp,382bp) .. controls (944.09bp,427.23bp) and (889.21bp,354.77bp)  .. (849.65bp,400bp) .. controls (844.38bp,406.02bp) and (844.24bp,412.11bp)  .. (849.65bp,418bp) .. controls (881.48bp,452.66bp) and (1019bp,414.04bp)  .. (1060.6bp,436bp) .. controls (1091.1bp,452.07bp) and (1081.3bp,476.53bp)  .. (1109.6bp,496bp) .. controls (1130.9bp,510.55bp) and (1149.6bp,493.18bp)  .. (1164.6bp,514bp) .. controls (1169.3bp,520.48bp) and (1169.8bp,525.87bp)  .. (1164.6bp,532bp) .. controls (1142.6bp,558.33bp) and (1046bp,566.89bp)  .. (node_18);
%   \draw (916.65bp,409bp) node { ($l_G$, $u_G$, $\lambda_G$)};
%   \draw [->,solid] (node_18) ..controls (999.92bp,562.32bp) and (1026.7bp,552.6bp)  .. (1040.6bp,532bp) .. controls (1047.6bp,521.72bp) and (1044.5bp,509.84bp)  .. (node_5);
%   \draw (1102.6bp,523bp) node { min(D,wtr4+1)};
%   \draw [->,solid] (node_0) ..controls (262.14bp,230.25bp) and (274.64bp,220.79bp)  .. (282.65bp,208bp) .. controls (287.37bp,200.47bp) and (288.77bp,191.2bp)  .. (node_16);
%   \draw (353.65bp,199bp) node { ($l_C$, $u_C$, $\lambda_C$)};
%   \draw [->,solid] (node_6) ..controls (884.99bp,498.11bp) and (892.8bp,506.21bp)  .. (899.65bp,514bp) .. controls (907.36bp,522.77bp) and (915.3bp,532.73bp)  .. (node_18);
%   \draw (937.65bp,523bp) node { $wob_2$};
%   \draw [->,solid] (node_10) ..controls (1184.6bp,438.31bp) and (1175.7bp,428.94bp)  .. (1170.6bp,418bp) .. controls (1165.9bp,407.73bp) and (1170bp,397.83bp)  .. (node_13);
%   \draw (1181.6bp,409bp) node { w};
%   \draw [->,solid] (node_18) ..controls (820.66bp,567.2bp) and (587.55bp,557.38bp)  .. (564.65bp,532bp) .. controls (551.56bp,517.5bp) and (561.64bp,504.71bp)  .. (node_1);
%   \draw (625.15bp,523bp) node { ($l_B$,$u_B$,$\lambda_B$)};
%   \draw [->,solid] (node_18) ..controls (1047.3bp,562.87bp) and (1200.9bp,548.8bp)  .. (1217.6bp,532bp) .. controls (1224.6bp,525bp) and (1227.9bp,515.33bp)  .. (node_10);
%   \draw (1285.6bp,523bp) node { min(D,wtr1+1)};
%   \draw [->,solid] (node_3) ..controls (188.81bp,505.35bp) and (183.22bp,521.01bp)  .. (193.65bp,532bp) .. controls (218.03bp,557.68bp) and (741.2bp,567.86bp)  .. (node_18);
%   \draw (217.65bp,523bp) node { $wob_1$};
%   \draw [->,solid] (node_8) ..controls (396.05bp,487.39bp) and (426.46bp,499.5bp)  .. (451.65bp,514bp) .. controls (462.9bp,520.48bp) and (462.56bp,527.26bp)  .. (474.65bp,532bp) .. controls (551.24bp,562.02bp) and (797.54bp,568.94bp)  .. (node_18);
%   \draw (496.15bp,523bp) node { wtr3};
%   \draw [->,solid] (node_2) ..controls (603.62bp,284.63bp) and (580.21bp,300.7bp)  .. (595.65bp,322bp) .. controls (599.35bp,327.11bp) and (607.48bp,331.9bp)  .. (node_19);
%   \draw (662.65bp,313bp) node { ($l_G$, $u_G$, $\lambda_G$)};
%   \draw [->,solid] (node_18) ..controls (780.96bp,568.75bp) and (332.56bp,560.39bp)  .. (275.65bp,532bp) .. controls (262.23bp,525.31bp) and (250.76bp,513.8bp)  .. (node_3);
%   \draw (299.65bp,523bp) node { $wob_1$};
%   \draw [->,solid] (node_7) ..controls (546.54bp,78.888bp) and (550.82bp,86.418bp)  .. (553.65bp,94bp) .. controls (565.76bp,126.53bp) and (563.61bp,137.8bp)  .. (557.65bp,172bp) .. controls (545.47bp,241.8bp) and (556.13bp,274.39bp)  .. (503.65bp,322bp) .. controls (479.54bp,343.87bp) and (452.64bp,314.31bp)  .. (432.65bp,340bp) .. controls (421.18bp,354.73bp) and (420.83bp,367.55bp)  .. (432.65bp,382bp) .. controls (458.2bp,413.24bp) and (485.18bp,382.71bp)  .. (521.65bp,400bp) .. controls (533.06bp,405.41bp) and (531.86bp,413.46bp)  .. (543.65bp,418bp) .. controls (581.44bp,432.55bp) and (876.16bp,410.54bp)  .. (907.65bp,436bp) .. controls (929.11bp,453.35bp) and (905.59bp,475.13bp)  .. (923.65bp,496bp) .. controls (936.93bp,511.36bp) and (954.47bp,497.05bp)  .. (965.65bp,514bp) .. controls (971.02bp,522.15bp) and (969.69bp,531.81bp)  .. (node_18);
%   \draw (543.15bp,313bp) node { wtr2};
%   \draw [->,solid] (node_9) ..controls (1403.9bp,617.6bp) and (1410.9bp,571.91bp)  .. (1413.6bp,532bp) .. controls (1414.2bp,524.02bp) and (1414.3bp,521.98bp)  .. (1413.6bp,514bp) .. controls (1410.3bp,470.95bp) and (1404.2bp,460.82bp)  .. (1398.6bp,418bp) .. controls (1392bp,367.48bp) and (1398bp,353.66bp)  .. (1386.6bp,304bp) .. controls (1374.6bp,251.51bp) and (1385.1bp,226.68bp)  .. (1345.6bp,190bp) .. controls (1340bp,184.73bp) and (1329bp,179.73bp)  .. (node_14);
%   \draw (1409.6bp,409bp) node { w};
%   \draw [->,solid] (node_12) ..controls (1091.3bp,220.35bp) and (1078.5bp,205.47bp)  .. (1089.6bp,190bp) .. controls (1093.3bp,184.93bp) and (1101.4bp,180.14bp)  .. (node_14);
%   \draw (1153.1bp,199bp) node { ($l_P$, $u_P$, $\lambda_P$)};
%   \draw [->,solid] (node_18) ..controls (887.94bp,562.18bp) and (861.41bp,552.45bp)  .. (847.65bp,532bp) .. controls (842.37bp,524.17bp) and (840.9bp,514.55bp)  .. (node_6);
%   \draw (871.65bp,523bp) node { $wob_2$};
% %
% \end{tikzpicture}
% % End of code
% }}
%  \caption{SNAKES Petri net rendering of the mobile phone example.
% }\label{fig:snakesbattery}  
% \end{figure}
% 



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Encoding into Timed Automata} \label{sec:timedauto}

In Section \ref{sec:reaction} we have hinted at the construction of a timed automaton coming directly from the marking graph of an  \andy network. Here we present another encoding that is syntax-driven which is not straightforward because of the management
of \obligatory rules. Unfortunately, even if the obtained automata is smaller, we cannot avoid it to be exponential at least in the number of activities.
We conclude this section showing that the semantics of \andy in terms of timed
automata is equivalent to the semantics in terms of high-level Petri
nets.


\paragraph{\bf Timed automata.}

A timed automaton is an annotated directed (and connected) graph, 
with an initial node and provided with a finite set of non-negative real 
variables called \emph{clocks}. 
Nodes (called \emph{locations}) are annotated with \emph{invariants} 
(predicates allowing to enter or stay in a location).
Arcs are annotated with \emph{guards}, 
\emph{communication labels}, and possibly with some clock \emph{resets}. 
Guards are conjunctions of elementary predicates of the form  
$x~\op~c$, where $\op\in\{>,\geq,=,>,\leq\}$ where $x$ is a clock and 
$c$ a (possibly parameterised) positive integer constant.
As usual, the empty conjunction is interpreted as true. 
The set of all guards and invariant predicates will be denoted by $G$. 

%In figures, locations will be represented by round nodes, the initial one having a double boundary. 

\begin{definition}\label{def:ta} A \emph{timed automaton} $\TA$
is a tuple $(L,l^0,X,\Sigma,\arcs,\inv)$, where 
\begin{itemize}
	\item $L$  is a set of locations with $l^0\in L$ the initial one, $X$ is the set of clocks, 
	\item $\Sigma=\Sigma^s\cup\Sigma^u\cup\Sigma^b$ is a set of communication labels, 
	where $\Sigma^s$ are synchronous, $\Sigma^u$ are synchronous and urgent, 
	and $\Sigma^b$ are broadcast ones,
	\item $\arcs \subseteq L \times (G \cup \Sigma \cup R) \times L$ 
is a set of arcs between locations with a guard in $G$, 
a communication label in $\Sigma\cup\{\epsilon\}$, and a set of clock resets in $R=2^X$;
for all $a\in\Sigma^u$, we require the guard to be $\true$; 
  \item $\inv: L \rightarrow G$ assigns invariants to locations. 
\end{itemize}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

It is possible to define a synchronised product of a set of timed automata 
that work and synchronise in parallel. 
The automata are required to have disjoint sets of locations, but
may share clocks and communication labels which are used for synchronisation. 
We define three communication policies: 
\begin{itemize}
	\item \emph{synchronous} communications through
		labels $a\in\Sigma^s$ that require all the automata having label $a$  
		to synchronise on $a$; 
	\item \emph{synchronous urgent} communications through 
		labels $u\in\Sigma^u$ that are synchronous as above but \emph{urgent} meaning that
		there will be no delay if transition with label $u$ can be taken;
  \item \emph{broadcast} communications through labels $b!,b?\in\Sigma^b$ meaning that
	a set of automata can synchronise if one is emitting;
	notice that, a process can always emit (\eg $b!$) 
	and the receivers ($b?$) must synchronise if they can.
\end{itemize}

The synchronous product $\TA_1\parallel \ldots \parallel \TA_n$ 
of timed automata, where for each $j\in[1,\ldots,n]$, 
$\TA_j = (L_j, l^0_j,X_j,\Sigma_j,\arcs_j,\inv_j)$ and all $L_j$ are 
pairwise disjoint sets of locations is
the timed automaton $\TA=(L, l^0,X,\Sigma,\arcs,\inv)$ such that:
\begin{itemize}
\item $L=L_1\times\ldots\times L_n$ and $l^0=(l^0_1,\ldots,l^0_n)$, 
$X=\bigcup_{j=1}^n X_j$, $\Sigma=\bigcup_{j=1}^n \Sigma_j$,
\item $\forall l=(l_1, \ldots, l_n)\in L\colon \inv(l) = \bigwedge_j \inv_j(l_j)$,
\item $\arcs$ is the set of arcs 
$(l_1, \ldots, l_n) \stackrel{g,a,r}{\longrightarrow} (l'_1, \ldots, l'_n)$
such that (where for each $a\in\Sigma^s\cup\Sigma^u, 
S_a=\{j\mid 1\leq j \leq n, a\in \Sigma^s_j\cup\Sigma^u_j\}$):
	for all $1\leq j \leq n$, if $j\not\in S_a$, then $l_j'=l_j$, otherwise
	there exist $g_j$ and $r_j$ such that 
	$l_j \stackrel{g_j,a,r_j}{\longrightarrow} l_j'\in E_j$; $g=\bigwedge_{j\in S_a} g_j$
	and $r=\bigcup_{j\in S_a} r_j$.
\end{itemize}

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is that of the underlying timed automaton $\TA$
(synchronising on synchronous and broadcast communication labels) as recalled below, 
with the following notations. 
A location is a vector $l = (l_1, \ldots, l_n)$. 
We write $l[l'_j/l_j, j\in S]$ to denote the location $l$ in which the 
$j$th element $l_j$ is replaced by $l'_j$, for all $j$ in some set $S$.
A valuation is a function $\nu$ from the set of clocks to the non-negative reals. 
Let $\mathbb{V}$ be the set of all clock valuations, and $\nu_0(x) = 0$ 
for all $x \in X$.  
We shall denote by $\nu\vDash F$ the fact that the valuation $\nu$ 
satisfies (makes true) the formula $F$.
If $r$ is a clock reset, we shall denote by $\nu[r]$ 
the valuation obtained after applying clock reset $r\subseteq X$ to $\nu$; 
and if $d\in\mathbb{R}_{> 0}$ is a delay, 
$\nu+d$ is the valuation such that, for any clock $x\in X$, 
$(\nu+d)(x)=\nu(x)+d$.

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is defined as a timed transition system $(S,s_0,\rightarrow)$,
where $S = (L_1 \times,\ldots\times L_n) \times \mathbb{V}$ is the set of states, 
$s_0 = (l^0, \nu_0)$ is the initial state, and 
$\rightarrow \subseteq S \times S$ is the transition relation defined by:
\begin{itemize}	
	%\item (silent): $(l,\nu) \rightarrow (l',\nu')$ 
	%if there exists $l_i \stackrel{g,~,r}{\longrightarrow} l'_i$, for some $i$, 
	%such that $l'=l[l'_i/l_i]$, $\nu\vDash g$ 
	%and $\nu'=\nu[r]$, 
	\item (sync): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if 
	there exist arc $l \stackrel{g,a,r}{\longrightarrow} l'\in \arcs$ 
	such that $\nu\vDash g$, $\nu'=\nu[r]$,
	for $S_a=\{j\mid 1\leq j\leq n, a\in\Sigma^s_j\}$, 
	$l'=l[l'_j/l_j, j\in S_a]$, 
	and there is no enabled transition with urgent communication label
	from $(\bar{l},\nu)$;
	
	\item (urgent): as (sync) but $a\in\Sigma^u$ and there is no delay
	if transition with urgent communication label can be taken;
	 
	\item (broadcast): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if
	there exist an output arc $l_j \stackrel{g_j,b!,r_j}{\longrightarrow} l_j'\in \arcs_j$ 
	and a (possibly empty) set of input arcs of the form
	$l_k \stackrel{g_k,b?,r_k}{\longrightarrow} l_k'\in \arcs_k$ such that 
	for all $k\in K=\{k_1,\ldots,k_m\}\subseteq\{l_1,\ldots,l_n\}\setminus\{l_j\}$,
	the size of $K$ is maximal, $\nu\vDash \bigwedge_{k\in K\cup\{j\}} g_k$,
	$l'=l[l'_k/l_k, k\in K\cup\{j\}]$ and $\nu'=\nu[r_k, k\in K\cup\{j\}]$;
	
	\item (timed): $(l,\nu)\rightarrow (l,\nu+d)$ if $\nu+d\vDash \inv(l)$. 
\end{itemize} 
%\begin{figure}[htbp]
%\centering
%\subfigure[$\TA_1\parallel \TA_2$]{
Here we exemplify timed automata usage: 
consider for instance the network of timed automata $\TA_1$ and $\TA_2$ with synchronous (non urgent) communications only:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.8, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$\stackrel{l_1}{x < 2}$}; 
\node[location]  at (4,0) (l2) {$\stackrel{l_2}{x < 2}$};
\node[left] at (-4,0) {$\TA_1$};
\node[location,double] at (0,-2) (l3) {$\stackrel{l_3}{\emptyset}$};
\node[location] at (4,-2) (l4) {$\stackrel{l_4}{\emptyset}$};
\draw[->, rounded corners] (l2) -- (5,-.5) -- (5.5,-.5) -- node[midway,right] 
				{$x>0;b;\emptyset$}  (5.5,.5) -- (5,.5)-- (l2) ;

\node[left] at (-4,-2) {$\TA_2$};
\draw[->] (l1) -- (l2) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l3) -- (l4) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l3) -- (-1,-2.5) -- (-1.5,-2.5) -- node[midway,left] 
				{$\true;a;\{x\}$}  (-1.5,-1.5) -- (-1,-1.5)-- (l3) ;
\end{tikzpicture}
\end{center}
%}
%%%
%\subfigure[$sync(\TA_1\parallel \TA_2)$]{
whose behaviour is given by their synchronised product $\TA_1\parallel \TA_2$:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.9, yscale=.6,every node/.style={scale=0.7}]
\node[location]  at (0,0) (l14) {$\stackrel{(l_1,l_4)}{x < 2}$};
\node[location,double] at (3,0) (l13) {$\stackrel{(l_1,l_3)}{x < 2}$}; 
\node[location] at (6,0) (l23) {$\stackrel{(l_2,l_3)}{x < 2}$};
\node[location] at (9,0) (l24) {$\stackrel{(l_2,l_4)}{x < 2}$};
\draw[->, rounded corners] (l23) -- (5.5,1) -- (5.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (6.5,1.5) -- (6.5,1)-- (l23) ;
\draw[->] (l13) -- (l14) node[midway,above] {$x=1;c;\emptyset$};
\draw[->] (l13) -- (l23) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l23) -- (l24) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l24) -- (8.5,1) -- (8.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (9.5,1.5) -- (9.5,1)-- (l24) ;
\end{tikzpicture}
\end{center}
%}
%%%
%HK doit être modifié pour inclure des canaux broadcast
%\subfigure[A possible run]{
and where a possible run is:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node at (0,0) (e1) {$[(l_1,l_3);x=0]$}; // t+1
\node at (2,0) (e2) {$[(l_1,l_3);x=1]$}; // a
\node at (4,0) (e3) {$[(l_2,l_3);x=0]$}; // t+.5
\node at (6,0) (e4) {$[(l_2,l_3);x=.5]$}; // b
\node at (8,0) (e5) {$[(l_2,l_3);x=.5]$}; // t+.5
\node at (10,0) (e6) {$[(l_2,l_4);x=1]$}; 
\draw[->] (e1) -- (e2) ;
\draw[->] (e2) -- (e3) ;
\draw[->] (e3) -- (e4) ;
\draw[->] (e4) -- (e5) ;
\draw[->] (e5) -- (e6) ;
\end{tikzpicture}
\end{center}
%}
%\caption{A network of timed automata with a possible run.}
%\label{fig:ta}
%\end{figure}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{\bf Encoding into timed automata.}
We are now ready to introduce the encoding of the high-level Petri net formalisation of $\andy$, to this aim we need to add some notation:

 \begin{newnotation}
Let $\Tag=\{\beta_1,\ldots,\beta_n\}$ be the set of all \obligatory activities identifiers from $\Syn$,
ordered alphabetically, i.e., $\beta_i<\beta_j$ if $i<j$. 
We denote by 
\[
\Tag^{\circledast}=\{ seq(h) \mid h\in \mathcal{P}(\Tag) \wedge h\neq\emptyset \} \cup \{ \varepsilon\},
\] 
the set of sequences $seq(h)$ obtained by concatenating the identifiers in non-empty subsets $h$ of $\Tag$, where for each $h=\{\beta_{i_1},\ldots,\beta_{i_m}\mid \forall j,k:~ i_j<i_k \}\in \mathcal{P}(\Tag)$, $seq(h)=\beta_{i_1}\cdots \beta_{i_m}$. We assume that if $\Tag^{\circledast}=\{h_1 \mydots h_k\}$, then the $h_i$'s are ordered by decreasing length and alphabetically in such a way that $h_1=\beta_1\cdots\beta_{|\Tag|}$ and $h_k = \varepsilon$. 

Moreover, $\beta_i=h[i]$ is the identifier at the $i$-position, and  $h=h_1-h_2$ is  the sequence of identifier in $h_1$ without those in $h_2$.
  %Let $Lab$ be a set of labels, we denote with 
  %$$Lab^{\circledast} = \{x_1 \cdots x_n \mid n \in [1..|Lab|], \forall i,j \in [1..n], x_i \in Lab \wedge x_i < x_j  \} \cup \{ \varepsilon\}$$ 
  %the set of labels obtained by concatenating in alphabetical order ($<$) the labels in $Lab$, using them at most once.  
  %
  %Labels in $Lab^{\circledast} $ can be alphabetically ordered from the longest to $\varepsilon$ thus we denote  $Lab^{\circledast} = \{t_1 \mydots t_n \} $ where $t_1$ is the word composed of all labels in $Lab$ and $t_n = \varepsilon$. 
 \end{newnotation}

 The encoding of an $\andy$ network is the synchronised product of one timed automaton for each entity in \entities  together with a set of auxiliary automata that are used to handle \potential and \obligatory activities.  
 The idea is that the global state of an \andy network is divided into its local counterparts represented by state of entities (\ie their levels). Thus for each entity $\entity$ we build a timed automaton $\TA(\entity, \level{\entity})$ which has as many locations as the levels in $\entity$. Auxiliary automata are used to implement the encoding of places $p_{\rho}$ ($\TA(\rho)$ for $\rho \in \Syn \cup \Reac$) and to realise time progression together with \obligatory activities ($\TA_{\tick}$). 
 More formally:
 
 \begin{definition} Given an \andy network $(\entities, \Syn, \Reac)$, with initial expression level $\level{\entity}$ for each $\entity \in \entities$, the corresponding timed automata encoding is 
 \[\enc{(\entities, \Syn, \Reac)} = \prod_{\entity \in \entities} \TA(\entity,\level{\entity}) \parallel \prod_{\alpha \in  \Reac} \TA(\alpha) \parallel \prod_{\beta \in \Syn} \TA(\beta) \parallel \TA_{\tick} \]  
 where $\TA(\entity, \level{\entity})$, $\TA(\alpha)$,$\TA(\beta)$  and $\TA_{\tick}$ are defined next. In the following we assume $ \Tag $ to be the set of identifiers of \obligatory activities in $\Syn$. 
 \paragraph{\bf Entities.}
 $\TA(\entity, \level{\entity}) = (L_{\entity},l^0_{\entity},X_{\entity},\Sigma_{\entity}, \arcs_{\entity} ,\inv_{\entity})$
  where:
  \begin{itemize}
   \item $L_{\entity}=\{l^{\entity}_i \mid i \in [0 \mydots \setlev_{\entity} ]\} \cup \{k_i^h,k_i^{d,h} \mid i \in [0 \mydots \setlev_{\entity} ], h\in \Tag^{\circledast} \}$ with  $l^0_{\entity} = l^{\entity}_{\level{\entity}}$
   \item $X_{\entity}=\{\birth^{\entity}_i, \refr^{\entity}_i \mid i \in [0 \mydots \setlev_{\entity} ]\} \cup \{x_{\entity}\}$
   \item $\Sigma^s_{\entity} =  \{  \alpha \mid \alpha \text{ identifier of an activity in }  \Reac  \}$, $  \Sigma_{\entity}^b =  \Tag^{\circledast}$, $\Sigma_{\entity}^u =  \{\tick h \mid h \in \Tag^{\circledast} \} $ 
   \item $\arcs_{\entity} = \arcs_{\Reac} \cup \arcs_{\Syn}$ where 
$$
\arcs_{\Reac}\! =\! \{ l_j \xrightarrow{g(A_{\alpha}) \wedge g(I_{\alpha}) \wedge x_{\entity} = 0, \alpha, r} l_e \mid \entity_{A_{\alpha}} \leq j < \entity_{I_{\alpha}}, \alpha \in \Reac, \entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}  
$$
with  $j, e, \entity_{A_{\alpha}}$, and $\entity_{I_{\alpha}}$ are levels of $\entity$ defined as follows:
    
    $$\entity_{A_{\alpha}} = \begin{cases}
                \level{a} & \text{if } (\entity, \level{a}) \in {A_{\alpha}}     \\
                0 & \text{otherwise}
               \end{cases}
\qquad 
\entity_{I_{\alpha}} = \begin{cases}
               \level{i} & \text{if } (\entity, \level{i}) \in {I_{\alpha}}\\
                \setlev_{\entity} & \text{otherwise}
               \end{cases}
$$

$$ g(A_{\alpha}) = \begin{cases}
\birth^{\entity}_{\level{a}} \geq \dur{\alpha} & \text{if } (\entity, \level{a}) \in A_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
\ 
g(I_{\alpha}) = \begin{cases}
\birth^{\entity}_{\level{i}} \geq \dur{\alpha} & \text{if } (\entity, \level{i}) \in I_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
$$

$$m = \begin{cases}
               \max(0, \min(j+v, \setlev_{\entity}-1)) & \text{if } (\entity, v) \in R_{\alpha} \\
                j & \text{otherwise}
               \end{cases}
$$

$$r = \begin{cases}
        \emptyset & \text{if } (\entity, v) \not \in R_{\alpha}  \\
        \{u^\entity_m,\} \cup \{\birth_x^{\entity} \mid x \in [j+1,m]\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge m-j>0\\
        \{u^\entity_m,\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge m-j=0\\
        \{u^\entity_m,\} \cup \{\birth_x^{\entity} \mid x \in [m+1,j]\} & \text{if } (\entity, v) \in R_{\alpha}  \wedge m-j<0
      \end{cases}
$$
$$
\begin{array}{ll}
 \arcs_{\Syn} = & \{ l_j \xrightarrow{g(d)\wedge g , h?, \emptyset} k_j^{d,h},  \mid  j \in [0\mydots\setlev_{\entity}-1], h\in \Tag^{\circledast}\} \ \cup \\
               & \{ l_j \xrightarrow{\neg g(d)\wedge g , h?, \emptyset} k_j^h,  \mid  j \in [0\mydots\setlev_{\entity}-1], h\in \Tag^{\circledast}\} \ \cup \\
              & \{ k_j^{d,h} \xrightarrow{\true, h', r \cup \{x_{\entity}\} } l_e,  \mid  j \in [0\mydots\setlev_{\entity}-1], h,h' \in \Tag^{\circledast}, h<h' \}\ \cup \\ 
              & \{ k_j^h \xrightarrow{\true, \tick h', r'\cup \{x_{\entity}\} } l_e',  \mid  j \in [0\mydots\setlev_{\entity}-1], h,h' \in \Tag^{\circledast}, h<h' \}
\end{array}
$$
where
$$\begin{array}{lcl}
   g & = & \! \bigwedge_{k=1}^{n} g(\beta_k)  \wedge \bigwedge_{k=1}^{m} \neg g(\beta'_m)\text{ for } h=\beta_1 \cdots \beta_n \text{ and } h_1- h= \beta'_1 \cdots \beta'_m \\
   g(\beta) & = & g'(A_\beta) \wedge g'(I_\beta) \text{ and } \beta= \activ{A_\beta}{I_\beta}{\dur{\beta}}{R_\beta}\\
   g(d) & = & u_j > \life_{\entity}(j)
  \end{array}
$$    


$$ g'(A_\beta) = \begin{cases}
j \geq \level{a} \wedge \birth^{\entity}_{\level{a}} \geq \dur{\beta} & \text{if } (\entity, \level{a}) \in A_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
g'(I_\beta) = \begin{cases}
j<\level{i} \wedge \birth^{\entity}_{\level{i}} \geq \dur{\beta} & \text{if } (\entity, \level{i}) \in I_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
\begin{array}{lcl}
m & = & \max(0, \min(\sum_{i\in[1 \mydots n]} f(h[i]') +j -1, \setlev_{\entity}-1)) \\
m' & = & \max(0, \min(\sum_{i\in[1\mydots n]} f(h[i]')+j, \setlev_{\entity}-1)) \\
 & & \mbox{ where } f(h[i]) = \begin{cases}
        v & \text{if }  (\entity, v) \in R_{\beta_i} \\
        0 & \text{otherwise} 
       \end{cases}
\end{array}
$$
\[
\begin{array}{ll}
r = &\begin{cases}
        \{u^\entity_m\} \cup \{\birth_x^{\entity} \mid x \in [j+1,m]\} & \text{if }  m-j>0\\
        \{u^\entity_m\} & \text{if }   m-j=0 \\
        \{u^\entity_m\} \cup \{\birth_x^{\entity} \mid x \in [m+1,j]\} & \text{if }   m-j<0     
      \end{cases}
      \\
r' = &\begin{cases}
        \{u^\entity_{m'}\} \cup \{\birth_x^{\entity} \mid x \in [j+1,m']\} & \text{if }  m'-j>0\\
        \{u^\entity_{m'}\} & \text{if }  \entity \in h'  \wedge m'-j=0 \\
        \{u^\entity_{m'}\} \cup \{\birth_x^{\entity} \mid x \in [m'+1,j]\} & \text{if }   m'-j<0 \\
        \emptyset & \text{if }  \entity \notin h' 
      \end{cases}
\end{array}
     \]
where $\entity \in h$ denotes formula: $\exists \beta_k=\activ{A_{\beta_k}}{I_{\beta_k}}{\dur{\beta_k}}{R_{\beta_k}}$ s.t. $h=\beta_1\cdots \beta_n, 1\leq k \leq n \wedge (\entity, v) \in R_{\beta_k}$ 
    
   \item $Inv_{\entity}(l^{\entity}_i) = \refr^{\entity}_i \leq \life_{\entity}(i)$ for all $i \in [0 \mydots \setlev_{\entity}]$
   
  \end{itemize}

  \paragraph{\bf \Potential activity.}
$\TA(\alpha) = (L_{\alpha},l^0_{\alpha},X_{\alpha},\Sigma_{\alpha},\arcs_{\alpha},\inv_{\alpha})$  for $\alpha \in \Reac$ where
  \begin{itemize}
  \item $L_{\alpha}=\{l_\alpha\}$,  $l^0_{\alpha} = \alpha$, $X_{\alpha}= \{w_{\alpha}\}$,  $\Sigma^s_{\alpha} = \{ \alpha \} $
  \item $\arcs_{\alpha} = \{ l_\alpha \xrightarrow{w_{\alpha} \geq  \dur{\alpha}, \alpha, \{ w_{\alpha}\}} l_\alpha \}$
  \item $\inv_{\alpha}(l_{\alpha}) = \true$.
  \end{itemize}
  
  \paragraph{\bf \Obligatory activity.} $\TA(\beta) = (L_{\beta},l^0_{\beta},X_{\beta},\Sigma_{\beta},\arcs_{\beta},\inv_{\beta})$  for $\beta \in \Syn$ where
  \begin{itemize}
   \item $L_{\beta}=\{l_\beta, l'_\beta\}$,  $l^0_{\beta} = l_\beta$,  $X_{\beta}= \{w_{\beta}\}$,  $\Sigma_{\beta}^b =  \Tag^{\circledast}$,  $
\Sigma_{\beta}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\beta} = \{ l_\beta \xrightarrow{w_{\beta} \geq  \dur{\beta}, h?, \emptyset} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \} \cup \{ l'_\beta \xrightarrow{\true, \tick h, \{w_{\beta}\}} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \}$
   \item $\inv_{\beta}(l_{\beta}) = \true$ and $\inv_{\beta}(l'_{\beta}) = \true$.
  
  \end{itemize}
  
  \paragraph{\bf Time.}  $\TA_{\tick} = (L_{\tick},l^0_{\tick},X_{\tick},\Sigma_{\tick},\arcs_{\tick},\inv_{\tick})$ where
  \begin{itemize}
   \item $L_{\tick}=\{l_h \mid h \in \Tag^{\circledast}\} \cup \{l_{\bot}\}$,  $l^0_{\tick} = l_{h_1}$,  $X_{\tick}= \{x\}$, $\Sigma_{\tick}^b =  \Tag^{\circledast}$, $ 
\Sigma_{\tick}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\tick} =\begin{array}{l}
 \{l_{h_i} \xrightarrow{x=1, h_i!, \emptyset } l_{h_i+1}, l_{h_i+1} \xrightarrow{\true, \tick h_i, \{x\} } l_{h_1} \mid h,  i \in [1\mydots n-1]   \}  \\
\cup \ \{ l_{h_n} \xrightarrow{x=1, h_n!, \emptyset } l_{\bot}, l_{\bot} \xrightarrow{\true, \tick\varepsilon, \{x\} } l_{h_1}   \}
                  \end{array}
$
   \item $\inv_{\tick}(l) = \true$ for all $l \in L_{\tick}$.
  
  \end{itemize}
  
  
  
 \end{definition}

 
  \begin{theorem}
The above encoding of  \andy network $(\entities, \Syn, \Reac)$
%its encoding $\enc{(\entities, \Syn, \Reac)}$, 
is correct and complete.\looseness=-1
\end{theorem}
\begin{proof}[Sketch]
 Follows by induction on the length of the run and from a case analysis on the transition performed. 
 
Some intuitions on the proof follows. For each entity $\entity$, the corresponding marking of place $p_{\entity}$, $M(p_{\entity})=\tuple{\lev_{\entity}, \refr_{\entity}, \birth_{\entity}}$, in the Petri net representation is encoded by    
 the state (location $l^{\entity}_{\lev_{\entity}}$ and valuations of clocks variables $\refr^{\entity}_{\lev_{\entity}}, \birth^{\entity}_i$ for $i \in [0\mydots\setlev_{\entity} -1]$) of each timed automaton $\TA(\entity, \level{\entity})$. Marking of places $p_{\rho}$ (for $\rho \in \Syn \cup \Reac$) is given by the valuation of clock $w_{\rho}$ in the corresponding timed automaton $\TA(\rho)$.
 
 Each transition of the Petri net is encoded by (a series of) timed automata arcs.
 For each transition $t_{\alpha}$ (corresponding to  \potential activity  $\alpha$) involving $\entity$ there is a (synchronous) arcs in the timed automaton $\TA(\entity, \level{\entity})$ whose guard describes its role in the activity (activator, inhibitor or result). Clock $w_{\alpha}$ in   $\TA(\alpha)$ implements the constraint that the activity $\alpha$ is performed at most once in the interval $\dur{\alpha} $:  $w_{\alpha} \geq \dur{\alpha}$. 
 This way, the synchronous product of all automata reconstructs the full guard of the activity $\alpha$ and  exactly one  transition in the synchronised product of automata corresponds to the firing of transition $t_{\alpha}$. The state reached after this transition coincides with the corresponding marking in the Petri net.
 
 Transition $t_c$ is trickier as time progression causes  decay but more importantly the simultaneous action of \obligatory activities.
 Notice that \obligatory activities concern the global state of an \andy network (the maximal set of enabled \obligatory activities has to be performed each time $t_c$ fires) but each sub-automaton of the synchronised automaton as only a partial/local information.  
 That is why, we need to introduce the auxiliary automaton $\TA_{\tick}$ that coordinates and gathers partial information from all  other automata.
 Thus, the implementation of $t_c$ has two phases. The first one gathers partial information, performs the selection of the largest set of enabled \obligatory activities and forces the time to progress in a discrete fashion;  the second phase completes the time progression and synchronises all timed automata communicating the chosen maximal set of \obligatory activities.
 Both phases are initiated by   automaton $\TA_{\tick}$ which has two types of arcs: broadcast ones for the first phase and urgent synchronous ones for the second (see Figure \ref{fig:tick}).
\begin{figure}[t]
\centering
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$l_{\beta_1\beta_2}$}; 
\node[location]  at (2,0) (l2) {$l_{\beta_1}$};
\node[location]  at (4,0) (l3) {$l_{\beta_2}$};
\node[location]  at (6,0) (l4) {$l_{\epsilon}$};
\node[location]  at (8,0) (l5) {$l_{\bot}$};
\draw[->] (l1) -- node[midway,above] {$\beta_1\beta_2!$} (l2) ;
\draw[->] (l2) -- node[midway,above] {$\beta_1!$} (l3) ;
\draw[->] (l3) -- node[midway,above] {$\beta_2!$} (l4) ;
\draw[->] (l4) -- node[midway,above] {$\epsilon!$} (l5) ;
\draw[->, rounded corners] (l2) -- node[midway,right] {$\tick\beta_1\beta_2$}(2,1.5) -- (1,1.5) --  (l1) ;
\draw[->, rounded corners] (l3) -- node[midway,right] {$\tick\beta_1$}(4,2) -- (1,2) --  (l1) ;
\draw[->, rounded corners] (l4) -- node[midway,right] {$\tick\beta_2$}(6,2.5) -- (1,2.5) --  (l1) ;
\draw[->, rounded corners] (l5) -- node[midway,right] {$\tick\epsilon$}(8,3) -- (1,3) --  (l1) ;

\end{tikzpicture}
\caption{The shape of timed automaton $\TA_\tick$ for $\Tag^\circledast=\{\beta_1\beta_2,\beta_1,\beta_2,\epsilon\}$, where $\tick\beta_1\beta_2$, $\tick\beta_1$, $\tick\beta_2$, $\tick\epsilon$ are all synchronous urgent communication labels.}
\label{fig:tick}
\end{figure}
More precisely, $\TA_{\tick}$ progressively interrogates the entities timed automata $\TA(\entity, \level{\entity})$ and the \obligatory activities automata $\TA(\beta_i)$ to ``compute'' for each automaton the maximal set of enabled \obligatory activities. This is obtained through broadcast arcs labelled with sequences of \obligatory activities identifiers $h\in\Tag^\circledast$, from the longest ($h=seq(\Tag)=\beta_1\cdots\beta_n$) to the shortest ($h=\epsilon$, \ie no \obligatory activity is enabled).
 As broadcast is a non blocking transition and because of the ordering on sequences in $\Tag^\circledast$, each entity automaton chooses its maximal set of \obligatory activities it is involved in. If it is necessary, it also performs decay. When all automata $\TA(\entity, \level{\entity})$ and $\TA(\beta_{i})$ have agreed on some sequence $h=\beta_{i_1} \mydots \beta_{i_m}$ (in the worst case $h$ is empty) the first phase is completed and $\{ \beta_{i_1},  \mydots,  \beta_{i_m}\}$ is the largest set of enabled \obligatory activities. The second phase is then implemented with an urgent synchronous arc synchronising all automata: $\TA_{\tick}$, $\TA(\entity, \level{\entity})$, for each $\entity \in \entities$, and $\TA(\beta_i)$, for $i\in [i_1 \mydots i_m]$.
 Notice that guards on broadcast transitions constraint the clocks to progress by one time unit at once.   
 As a consequence, at the end of the two phase algorithm, timed automata of entities and of places $p_{\rho}$ together with the  corresponding clocks valuations exactly encode the marking reached after firing $t_c$. 
 \qed
\end{proof}


\section{Blood glucose regulation}\label{sec:example}
Here we introduce another example:  \emph{glucose regulation} in human body (Figure \ref{fig:glucose}). This example shows that \andy model is not limited to genetic regulations but it may express other kinds of interactions. 
In the following, we are always referring to the process under normal circumstances in a healthy body.

Glucose regulation is a homeostatic process: \ie the rates of glucose in blood (\emph{glycemia}) must remain stable at what we call the equilibrium state. 
Glycemia is regulated by  two hormones: \emph{insulin} and  \emph{glucagon}. When glycemia rises (for instance as a result of the digestion of a meal), insulin  promotes the storing of glucose in muscles through the  glycogenesis process, thus decreasing the blood glucose levels. 
Conversely, when glycemia is critically low, glucagon  stimulates the process of glycogenolysis that increases the blood glucose level by transforming glycogen back into glucose.

 \begin{figure}[b]
\centering
\includegraphics[width=0.5\textwidth]{glucose.pdf} 
\caption{Glucose metabolism} \label{fig:glucose}
\end{figure}

We will focus on the assimilation of sweeteners: \ie sugars  or  artificial sweeteners such as aspartame. Whenever we eat something sweet either natural or artificial, the sweet sensation sends a signal to the brain (through \emph{neurotransmitters}) that in turns stimulates the production of insulin by pancreas. In the case of sugar, the digestion transforms food into nutrients (\ie glucose) that are absorbed by blood.
This way, sugar through digestion  increases glucose in blood giving the sensation of satiety. In case the income of glucose produces hyperglycemia,  the levels of glucose are promptly equilibrated by the intervention of insulin.
Unlike sugar, artificial sweeteners are not assimilated by the body, hence they do not increase the glucose levels in blood. Nevertheless  the insulin produced under the stimuli originated by the sweet sensation, although weak, can still cause the rate of glucose to drop engendering hypoglycemia. In response to that, the brain induces the  stimulus of \emph{hunger}. As a matter of fact this appears as an unwanted/toxic behaviour, indeed the assimilation of food (even if it contains aspartame) should calm hunger and induce satiety not the opposite. 

This schema suggests that we should consider four  levels for glycemia: low, hunger, equilibrium and high. Likewise for insulin we assume three levels: inactive, low and high. All other actors involved in glucose regulation, have only two  levels (inactive or active).  
In this example, duration do not play a fundamental role, for the sake of simplicity we have set all complementary activities such as production of insulin and glucagon,  to take the same amount of time, the signal to the brain is the fastest, and the decay of  glycemia values are much longer than the digestion process. 

Thus the set of involved entities is $$\entities = \{ Sugar, Aspartame, Glycemia, Glucagon, Insulin\}$$ and their expression levels and  corresponding decays are:
$$ 
\begin{array}{|lcl|}
\hline
  \mbox{levels} & \hspace{2cm} & \mbox{duration} \\
	\hline
	\setlev_{sugar}=\{0,1\} && \life_{sugar}(1)=2 \\
	\hline
  \setlev_{aspartame}=\{0,1\} && \life_{aspartame}(1)=2 \\
	\hline
  \setlev_{glycemia}=\{0,1,2,3\} \quad && \life_{glycemia}(1)=8 \\
  && \life_{glycemia}(2)=8\\
  && \life_{glycemia}(3)=8\\
	\hline
  \setlev_{glucagon}=\{0,1\} && \life_{glucagon}(1)=3\\
	\hline
  \setlev_{insulin}=\{0,1,2\} && \life_{insulin}(1)=3\\
  && \life_{insulin}(2)=3\\
	\hline
\end{array}
$$
 The levels of glycemia are: 0 corresponding to low, 1 to hunger, 2 to equilibrium and 3 to high. Likewise for insulin we have 0 that corresponds to inactive, 1 to low and 2 to high. All levels for the other species are 0 for inactive and 1 for active.
\hfill $\diamond$


The set of \potential activities $\Reac = \{\alpha_k=\activ{A_k}{I_k}{}{R_k} \mid k\in [1..9]\}$ for the glucose metabolism example  is:
$$\begin{array}{l l}
  \alpha_1: \ & \activ{(Sugar,1)}{\emptyset}{}{(Insulin,+1), (Glycemia,+1)} \\
 
	\alpha_2: & \activ{(Aspartame,1)}{ \emptyset }{}{(Insulin,+1)} \\
  
	\alpha_3 :& \activ{\emptyset}{(Glycemia,1)}{}{(Glucagon,+1)} \\
 % (\alpha_4) & \{(Glycemia,1)\} &\{(Glycemia,2)\}& \{(NT,+)\} &1\\
 % (\alpha_5) & \{(Glycemia,2)\} &\{(Glycemia,3)\}& \{(NT,-)\} &1\\

	\alpha_4 :& \activ{(Glycemia,3)}{ \emptyset}{}{ (Insulin,+1)} \\
  
	\alpha_5 :& \activ{(Insulin,2)}{ \emptyset}{}{(Glycemia,-1)} \\
 
	\alpha_6 :& \activ{(Insulin,1),(Glycemia,3)}{\emptyset}{}{(Glycemia,-1)} \\
 
	\alpha_7 :& \activ{(Insulin,1)}{  (Glycemia,2)}{}{(Glycemia,-1)} \\
  
	\alpha_{8}: & \activ{(Glucagon,1)} {\emptyset}{}{(Glycemia,+1)}  
   \end{array}
 $$
$\alpha_1$ and $\alpha_2$ represent the assimilation of Sugar and Aspartame, respectively: while Aspartame only increases the level of Insulin, Sugar also increases Glycemia.  $\alpha_3$ takes care of hypoglycemia, \ie a Glycemia level equal to 0 (obtained by using $(Glycemia, 1)$ as inhibitor) engenders the production of Glucagon. On the contrary, hyperglycemia causes the production of Insulin ($\alpha_4$). The presence of Insulin lowers Glycemia (activities $\alpha_5, \alpha_6, \alpha_7$). In particular Insulin level equal to 1 plays a role in the decrease of Glycemia only in case of hyperglycemia $\alpha_6$ or hypoglycemia $\alpha_7$, otherwise the signal is not strong enough and we need Insulin at level 2 to see the effect on Glycemia ($\alpha_5$). Last activity describes the role of Glucagon which if active increases the level of Glycemia.

For this example, the set of \obligatory activities is empty. Observe now the behaviour of
$Glycemia$ in the following scenario:
$$
\begin{array}{ll}
 \text{initial state} & \tuple{3, 0}  \\
 \text{$8$ time units elapse, counter at level $3$ updates} & \tuple{3, 8} \\
 \text{one time unit elapses, $Glycemia$ decays} & \tuple{2, 0} \\
  \text{one time unit elapses, counter at level $2$ updates} & \tuple{2, 1}\\
  \text{activity $\alpha_5$ decreases $Glycemia$ level} & \tuple{1, 0} \\
  \text{$8$ time units elapse, counter at level $1$ updates} & \tuple{1, 8} \\
\text{one time unit elapses, $Glycemia$ decays} & \tuple{0, 0}\\
  \text{one time unit elapses, no effect since $\life_{glycemia}(0)=\omega$ \quad} & \tuple{0, 0}. \qquad \diamond
\end{array}
$$

Figure \ref{fig:randyglucose} shows a simplification of the \andy network $(\entities, \Reac, \emptyset)$. It focuses only on the activity schema linking inputs (\ie activators and inhibitors) to results. 
Each input arc is labeled with either  letter A or letter I denoting whether the input place is an activator or an inhibitor,  respectively. Likewise, each output arc is labeled with a + or a - to denote increase or decrease of product levels by 1.
For each activity transition $\alpha$, we have omitted place $q_{\alpha}$ and all arcs in the opposite direction. 
The numbers inside each transition refers to the corresponding activity.


\begin{figure}[ht]
\centering
\begin{tikzpicture}[xscale=1.2, yscale=1.3, node distance=1.5cm,>=stealth',bend angle=45,auto]

\tikzstyle{place}=[rectangle,rounded corners,draw,fill=blue!20,minimum size=7mm]


 \node [place, label = above: ] at (2,7) (sugar){$Sugar$};
 \node [place, label = above: ] at (6,7) (asp){$Aspartame$};
 \node [place, label = right: ] at (2,4) (glucose){$Glycemia$};
% \node [place, label = right: ] at (5,5) (nt){$Neurotransmitter$};
 %\node [place, label = left: ] at (0,2) (glycog){$Glycogenesis$};
% \node [place, label = right: ] at (4,2) (glycol){$Glycogenolysis$};
 \node [place, label = right: ] at (-2,4) (gluc){$Glucagon$}; 
 \node [place, label = right: ] at (6,4) (ins){$Insulin$}; 
 %\node [place, label = above: ] at (-1,5) (hunger){$Hunger$};
%\node [place, label = below: ] at (6,5) (clock){$Clock$};

\node [transition, label={ right:}] at (2,5.5) (tr1) {1}
  edge [pre]    node[left] {A}    (sugar)
  edge [ post]    node[above] {+}   (ins)
  edge [ post]    node[left] {+}   (glucose);
  
\node [transition, label={ right:}] at (6,5.5) (tr2) {2}
  edge [pre]    node[left] {A}    (asp)
  edge [post]    node[left] {+}   (ins);

  
  \node [transition, label={ right:}] at (0,4) (tr3) {3}
  edge [pre]    node[above] {I}    (glucose)
  edge [ post]    node[above] {+}   (gluc);
  
  
\node [transition, label={right:}] at (4,4) (tr4) {4}
  edge [pre]    node[above] {A}    (glucose)
  edge [post]    node[above] {+}   (ins);
  



 \node [transition, label={right:}] at (4,3) (tr5) {5}
   edge [pre]    node[above] {A}    (ins)
   edge [post]    node[above] {-}   (glucose);
   
   \node [transition, label={ right:}] at (4,2) (tr6) {6}
   edge [pre]    node[above] {A}    (glucose)
   edge [pre]    node[above] {A}    (ins)
   edge [post, bend left=30]    node[above] {-}   (glucose);
 

\node [transition, label={ right:}] at (4,1) (tr7) {7}
  edge [pre, bend left=35]    node[above] {I}    (glucose)
  edge [pre]    node[right] {A}    (ins)

  edge [post, bend left =60]    node[left] {-}   (glucose);

 
 \node [transition, label={ right:}] at (0,3) (tr8) {8}
  edge [pre]    node[below] {A}    (gluc)
  edge [post]    node[below] {+}   (glucose);

\end{tikzpicture}
 \caption{Simplified \andy network of glucose metabolism. } \label{fig:randyglucose}
\end{figure}


\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,rounded corners, draw,fill=blue!30,minimum size=7mm]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

% \node [place, label = right: $Glycogenesis$] at (3,-1) (glycog){};
 \node [place, label = above:$q_{glycemia}$ ] at (0,4) (gl){$(3,0)$}; 
 \node [place, label = below: $q_{insulin}$ ] at (0,0) (ins){$(0,0)$}; 
 %\node [place, label = below:$\qquad \ \Pclock$ ] at (0,2) (clock){};
 \node [place, label = right:$q_{\alpha_7}$ ] at (6,2) (qw){1};
 
\node [transition, label={ left:$L(t_c)$} ] at (-3,2) (tr1) {$t_c$}
  %edge [post,bend left=30]    node[below] {$z'$}    (clock)
  %edge [pre ]    node[below] {$z$}    (clock)
  edge [pre, bend left]    node[left] {\ $\quad \tuple{\lev_{g},\refr_{g}}$}    (gl)
  edge [post]    node[right] {$\tuple{\lev'_{g},\refr'_{g}}$}    (gl)
  edge [pre, bend right ]    node [left] { $\tuple{\lev_i,\refr_i}$ }    (ins)
  edge [post ]    node[right] {$\ \tuple{\lev'_i,\refr'_i}$ }    (ins);
  
\node [transition, label={ right:$L(t_{\alpha_7})$}] at (3,2) (tr8) {$t_{\alpha_7}$}
  edge [pre, bend left=30 ]    node[above] {\qquad \quad $\tuple{\lev_g,\refr_g}$}    (gl)
  edge [pre and post]    node[right] {$\ \tuple{\lev_i,\refr_i}$}    (ins)
  %edge [pre and post]    node[below] {$z$}    (clock)
  edge [post,bend right]    node[right] {
  $ \tuple{\lev'_{g},\refr'_{g}} $}   (gl)
    edge [pre, bend left]    node[below] {$w$}   (qw)
  edge [post,bend right]    node[above] {$0$}   (qw);
\end{tikzpicture}
 \caption{A portion of the \andy network of glucose metabolism with an initial marking. } \label{fig:zoomrandyglucose}
\end{figure}


Figure \ref{fig:zoomrandyglucose}, instead, shows a portion of the complete 
initially marked \andy network for the glucose metabolism example, focusing only on activity $\alpha_7$. 

The following properties can be expressed in CTL:

\begin{description}
 \item[Symptoms:] Is it possible to have an anomalous decrease of glucose levels in blood (revealing hypoglycemia)? 
$$\esiste \finally (Glycemia, 0)$$
% \item [Mode-of-action:] Recalling that the blood glucose regulation process normally maintains  glycemia at equilibrium (level $2$), is there an abnormal behavior leading to hypoglycemia?
%$$\esiste (\esiste \finally (Glycemia, 2) ~\until~ (\esiste \finally (Glycemia, 0)))$$
 \item [Causality:] Does assimilation of sweeteners cause hypoglycemia? 
$$\begin{array}{l}
\esiste \finally [((Sugar, 1) \vee (Aspartame, 1)) \wedge (Glycemia, 1)] \rightarrow  \all \finally (Glycemia,2)   
  \end{array}
 $$
\end{description}

For the second formula we  show two paths given as sequences of activities (abstracting away from time transitions), one that satisfy the formula and the other that contradicts it.
The first one corresponds to the assimilation of sugar. It induces an increase of the production of insulin and an augmentation of the blood glucose levels. Nonetheless the levels of insulin produced are not enough to cause the glycemia to drop and the formula is satisfied.
$$
\begin{array}{l}
(Sugar, 1), (Aspartame, 0), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\alpha_1}\\
(Sugar, 1), (Aspartame, 0), \mathbf{(Glycemia, 2)}, (Insulin, 1), (Glucagon, 0) 
\end{array}
 $$
 
Unlike previous path, the assimilation of aspartame causes only an increase of insulin. Unfortunately, this increment is sufficient to induce a decrease of blood glucose levels thus contradicting the formula above.
$$
\begin{array}{l}
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\alpha_2} \\ 
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 1), (Glucagon, 0) \xrightarrow{\alpha_7} \\
 (Sugar, 0), (Aspartame, 0), \mathbf{(Glycemia, 0)}, (Insulin, 1), (Glucagon, 0)
\end{array}
 $$
This illustrates the toxic behaviour caused by aspartame.





